/-
Copyright (c) 2025 Amelia Livingston. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Amelia Livingston
-/
module

public import Mathlib.RepresentationTheory.Homological.FiniteCyclic
public import Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

/-!
# Group homology of a finite cyclic group

Let `k` be a commutative ring, `G` a group and `A` a `k`-linear `G`-representation. Given
endomorphisms `φ, ψ : A ⟶ A` such that `φ ∘ ψ = ψ ∘ φ = 0`, denote by `Chains(A, φ, ψ)` the
periodic chain complex `... ⟶ A --φ--> A --ψ--> A --φ--> A --ψ--> A ⟶ 0`.

When `G` is finite and generated by `g : G`, then `P := Chains(k[G], N, ρ(g) - Id)` (with `ρ` the
left regular representation) is a projective resolution of `k` as a trivial representation.
In this file we show that for `A : Rep k G`, `(A ⊗ P)_G` is isomorphic to
`Chains(A, N, ρ_A(g) - Id)` as a complex of `k`-modules, and hence the homology of this complex
computes group homology.

## Main definitions

* `Rep.FiniteCyclicGroup.groupHomologyIso₀ A g hg`: given a finite cyclic group `G` generated by
  `g`, and a representation `A : Rep k G`, this is an isomorphism `H₀(G, A) ≅ Coker(ρ_A(g) - Id)`.
* `Rep.FiniteCyclicGroup.groupHomologyIsoOdd A g hg i hi`: given a finite cyclic group `G`
  generated by `g`, and a representation `A : Rep k G`, this is an isomorphism between `Hᵢ(G, A)`
  and the homology of `A --N--> A --(ρ(g) - Id)--> A` for all odd `i`.
* `Rep.FiniteCyclicGroup.groupHomologyIsoEven A g hg i hi`: given a finite cyclic group `G`
  generated by `g`, and a representation `A : Rep k G`, this is an isomorphism between `Hᵢ(G, A)`
  and the homology of `A --(ρ(g) - Id)--> A --N--> A` for all positive even `i`.

-/

@[expose] public section

universe v u

open CategoryTheory Representation Finsupp Limits

namespace Rep.FiniteCyclicGroup

variable {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep k G) (g : G)

open ModuleCat.MonoidalCategory in
/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
the period chain complex
`... ⟶ (A ⊗ₖ k[G])_G --⟦Id ⊗ N⟧--> (A ⊗ₖ k[G])_G --⟦Id ⊗ (ρ(g⁻¹) - 𝟙)⟧--> (A ⊗ₖ k[G])_G ⟶ 0`
is isomorphic as a complex in `ModuleCat k` to
`... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0`. -/
@[simps!]
noncomputable def coinvariantsTensorResolutionIso (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    (resolution k g⁻¹ ((@Subgroup.zpowers_inv G ..).symm ▸ hg)).complex.coinvariantsTensorObj A ≅
      moduleCatChainComplex A g :=
  HomologicalComplex.Hom.isoOfComponents
    (fun _ => (coinvariantsTprodLeftRegularLEquiv A.ρ).toModuleIso) fun i j h =>
    coinvariantsTensor_hom_ext (LinearMap.ext fun a => lhom_ext' fun g => LinearMap.ext_ring (by
    subst h
    by_cases hj : Even (j + 1)
    · simpa [hj, whiskerLeft_def, coinvariantsTensorMk,
        tensorObj_carrier, ofCoinvariantsTprodLeftRegular, Representation.norm,
        ← Module.End.mul_apply, ← map_mul, mul_comm g⁻¹]
        using Finset.sum_bijective _ (MulEquiv.inv G).bijective (by aesop) (by aesop)
    · simp [hj, whiskerLeft_def, coinvariantsTensorMk, tensorObj_carrier,
        ← Module.End.mul_apply, ← map_mul, mul_comm g⁻¹]))

/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, `H₀(G, A)` is isomorphic
to the cokernel of `ρ(g) - Id(A)`. -/
noncomputable abbrev groupHomologyIso₀ (hg : ∀ x, x ∈ Subgroup.zpowers g) :
    groupHomology A 0 ≅ ModuleCat.of k (_ ⧸ (LinearMap.range (applyAsHom A g - 𝟙 A).hom.hom)) :=
  groupHomology.H0Iso A ≪≫ (Submodule.quotEquivOfEq _ _ (by
    simp [Representation.FiniteCyclicGroup.coinvariantsKer_eq_range A.ρ g hg])).toModuleIso

variable [DecidableEq G]

/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, `Hᵢ(G, A)` is isomorphic
to the homology of the short complex of `k`-modules `A --(ρ(g) - 𝟙)--> A --N--> A` when `i` is
nonzero and even. -/
noncomputable def groupHomologyIsoEven
    (hg : ∀ x, x ∈ Subgroup.zpowers g) (i : ℕ) [h₀ : NeZero i] (hi : Even i) :
    groupHomology A i ≅ (subCompNormHom A g).homology :=
  groupHomologyIso A i (resolution k g⁻¹ <| (@Subgroup.zpowers_inv G ..).symm ▸ hg) ≪≫
  (HomologicalComplex.homologyMapIso (coinvariantsTensorResolutionIso A g hg) i) ≪≫
  HomologicalComplex.alternatingConstHomologyIsoEven A.V (by ext; simp) (by ext; simp) _ (by aesop)
    (by induction i generalizing h₀ with | zero => exact (NeZero.ne 0 rfl).elim | succ n _ => simp)
    hi

/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, this is the quotient map
`Ker(N) ⟶ Ker(N)/Im(ρ(g) - Id(A)) ≅ Hᵢ(G, A)` for any nonzero even `i`. -/
noncomputable abbrev groupHomologyπEven
    (hg : ∀ x, x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) :
    ModuleCat.of k (LinearMap.ker A.ρ.norm) ⟶ groupHomology A i :=
  (ShortComplex.moduleCatCyclesIso <| subCompNormHom A g).inv ≫
    ShortComplex.homologyπ _ ≫ (groupHomologyIsoEven A g hg i hi).inv

lemma groupHomologyπEven_eq_zero_iff (hg : ∀ x, x ∈ Subgroup.zpowers g)
    (i : ℕ) [NeZero i] (hi : Even i) (x : LinearMap.ker A.ρ.norm) :
    groupHomologyπEven A g hg i hi x = 0 ↔
      x.1 ∈ LinearMap.range (applyAsHom A g - 𝟙 A).hom.hom := by
  simp [groupHomologyπEven, map_eq_zero_iff _ ((ModuleCat.mono_iff_injective _).1 inferInstance),
    ShortComplex.moduleCatToCycles, -LinearMap.mem_range, LinearMap.range_codRestrict]

lemma groupHomologyπEven_eq_iff (hg : ∀ x, x ∈ Subgroup.zpowers g)
    (i : ℕ) [NeZero i] (hi : Even i) (x y : LinearMap.ker A.ρ.norm) :
    groupHomologyπEven A g hg i hi x = groupHomologyπEven A g hg i hi y ↔
      x.1 - y.1 ∈ LinearMap.range (applyAsHom A g - 𝟙 A).hom.hom := by
  rw [← sub_eq_zero, ← map_sub, groupHomologyπEven_eq_zero_iff, AddSubgroupClass.coe_sub]

/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, `Hⁱ(G, A)` is isomorphic
to the homology of the short complex of `k`-modules `A --N--> A --(ρ(g) - 𝟙)--> A` when `i` is
odd. -/
noncomputable def groupHomologyIsoOdd (hg : ∀ x, x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) :
    groupHomology A i ≅ (normHomCompSub A g).homology :=
  groupHomologyIso A i (resolution k g⁻¹ <| (@Subgroup.zpowers_inv G ..).symm ▸ hg) ≪≫
  (HomologicalComplex.homologyMapIso (coinvariantsTensorResolutionIso A g hg) i) ≪≫
  HomologicalComplex.alternatingConstHomologyIsoOdd A.V (by ext; simp) (by ext; simp) (by aesop)
    (by simp) (by rcases hi with ⟨j, rfl⟩; simp) hi

/-- Given a finite cyclic group `G` generated by `g` and `A : Rep k G`, this is the quotient map
`Ker(ρ(g) - Id(A)) ⟶ Ker(ρ(g) - Id(A))/Im(N) ≅ Hᵢ(G, A)` for any odd `i`. -/
noncomputable abbrev groupHomologyπOdd (hg : ∀ x, x ∈ Subgroup.zpowers g) (i : ℕ) (hi : Odd i) :
    ModuleCat.of k (LinearMap.ker (applyAsHom A g - 𝟙 A).hom.hom) ⟶ groupHomology A i :=
  (ShortComplex.moduleCatCyclesIso <| normHomCompSub A g).inv ≫
    ShortComplex.homologyπ _ ≫ (groupHomologyIsoOdd A g hg i hi).inv

lemma groupHomologyπOdd_eq_zero_iff (hg : ∀ x, x ∈ Subgroup.zpowers g)
    (i : ℕ) (hi : Odd i) (x : LinearMap.ker (applyAsHom A g - 𝟙 A).hom.hom) :
    groupHomologyπOdd A g hg i hi x = 0 ↔ x.1 ∈ LinearMap.range A.ρ.norm := by
  simp [groupHomologyπOdd, map_eq_zero_iff _ ((ModuleCat.mono_iff_injective _).1 inferInstance),
    ShortComplex.moduleCatToCycles, -LinearMap.mem_range, LinearMap.range_codRestrict]

lemma groupHomologyπOdd_eq_iff (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g)
    (A : Rep k G) (i : ℕ) (hi : Odd i) (x y : LinearMap.ker (applyAsHom A g - 𝟙 A).hom.hom) :
    groupHomologyπOdd A g hg i hi x = groupHomologyπOdd A g hg i hi y ↔
      x.1 - y.1 ∈ LinearMap.range A.ρ.norm := by
  rw [← sub_eq_zero, ← map_sub, groupHomologyπOdd_eq_zero_iff, AddSubgroupClass.coe_sub]

end FiniteCyclicGroup
end Rep
